Proving equational and inductive theorems by completion and embedding techniques
Identifieur interne : 00DA46 ( Main/Exploration ); précédent : 00DA45; suivant : 00DA47Proving equational and inductive theorems by completion and embedding techniques
Auteurs : J. Avenhaus [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The Knuth-Bendix completion procedure can be used to transform an equational system into a convergent rewrite system. This allows to prove equational and inductive theorems. The main draw back of this technique is that in many cases the completion diverges and so produces an infinite rewrite system. We discuss a method to embed the given specification into a bigger one such that the extended specification allows a finite "parameterized" description of an infinite rewrite system of the base specification. The main emphasis is in proving the correctness of the approach. Examples show that in many cases the Knuth-Bendix completion in the extended specification stops with a finite rewrite system though it diverges in the base specification. This indeed allows to prove equational and inductive theorems in the base specification.
Url:
DOI: 10.1007/3-540-53904-2_110
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003275
- to stream Istex, to step Curation: 003234
- to stream Istex, to step Checkpoint: 003113
- to stream Main, to step Merge: 00E324
- to stream Main, to step Curation: 00DA46
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proving equational and inductive theorems by completion and embedding techniques</title><author><name sortKey="Avenhaus, J" sort="Avenhaus, J" uniqKey="Avenhaus J" first="J." last="Avenhaus">J. Avenhaus</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:D50352A00042BAC28F326B0E9C4221BE536F10CB</idno><date when="1991" year="1991">1991</date><idno type="doi">10.1007/3-540-53904-2_110</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VHNB6H2M-T/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003275</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003275</idno><idno type="wicri:Area/Istex/Curation">003234</idno><idno type="wicri:Area/Istex/Checkpoint">003113</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003113</idno><idno type="wicri:doubleKey">0302-9743:1991:Avenhaus J:proving:equational:and</idno><idno type="wicri:Area/Main/Merge">00E324</idno><idno type="wicri:Area/Main/Curation">00DA46</idno><idno type="wicri:Area/Main/Exploration">00DA46</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proving equational and inductive theorems by completion and embedding techniques</title><author><name sortKey="Avenhaus, J" sort="Avenhaus, J" uniqKey="Avenhaus J" first="J." last="Avenhaus">J. Avenhaus</name><affiliation wicri:level="4"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Department of Computer Science, University of Kaiserslautern, 6750, Kaiserslautern</wicri:regionArea><orgName type="university">Université technique de Kaiserslautern</orgName><placeName><settlement type="city">Kaiserslautern</settlement><region type="land" nuts="2">Rhénanie-Palatinat</region></placeName></affiliation><affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The Knuth-Bendix completion procedure can be used to transform an equational system into a convergent rewrite system. This allows to prove equational and inductive theorems. The main draw back of this technique is that in many cases the completion diverges and so produces an infinite rewrite system. We discuss a method to embed the given specification into a bigger one such that the extended specification allows a finite "parameterized" description of an infinite rewrite system of the base specification. The main emphasis is in proving the correctness of the approach. Examples show that in many cases the Knuth-Bendix completion in the extended specification stops with a finite rewrite system though it diverges in the base specification. This indeed allows to prove equational and inductive theorems in the base specification.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Rhénanie-Palatinat</li></region><settlement><li>Kaiserslautern</li></settlement><orgName><li>Université technique de Kaiserslautern</li></orgName></list><tree><country name="Allemagne"><region name="Rhénanie-Palatinat"><name sortKey="Avenhaus, J" sort="Avenhaus, J" uniqKey="Avenhaus J" first="J." last="Avenhaus">J. Avenhaus</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00DA46 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00DA46 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:D50352A00042BAC28F326B0E9C4221BE536F10CB
|texte= Proving equational and inductive theorems by completion and embedding techniques
}}
| This area was generated with Dilib version V0.6.33. |  |